0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 24 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 151 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
goalF_in_gaa(s(T16), T10, T11) → U5_gaa(T16, T10, T11, s2lA_in_ga(T16, X32))
s2lA_in_ga(s(T24), .(X66, X67)) → U1_ga(T24, X66, X67, s2lA_in_ga(T24, X67))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T24, X66, X67, s2lA_out_ga(T24, X67)) → s2lA_out_ga(s(T24), .(X66, X67))
U5_gaa(T16, T10, T11, s2lA_out_ga(T16, X32)) → goalF_out_gaa(s(T16), T10, T11)
goalF_in_gaa(s(T16), T42, T43) → U6_gaa(T16, T42, T43, s2lA_in_ga(T16, T41))
U6_gaa(T16, T42, T43, s2lA_out_ga(T16, T41)) → U7_gaa(T16, T42, T43, appendD_in_agaa(X93, T41, T42, X92))
appendD_in_agaa(X117, T57, T58, .(X117, X118)) → U4_agaa(X117, T57, T58, X118, appendB_in_gaa(T57, T58, X118))
appendB_in_gaa([], T65, .(T65, [])) → appendB_out_gaa([], T65, .(T65, []))
appendB_in_gaa(.(T72, T75), T76, .(T72, X140)) → U2_gaa(T72, T75, T76, X140, appendB_in_gaa(T75, T76, X140))
U2_gaa(T72, T75, T76, X140, appendB_out_gaa(T75, T76, X140)) → appendB_out_gaa(.(T72, T75), T76, .(T72, X140))
U4_agaa(X117, T57, T58, X118, appendB_out_gaa(T57, T58, X118)) → appendD_out_agaa(X117, T57, T58, .(X117, X118))
U7_gaa(T16, T42, T43, appendD_out_agaa(X93, T41, T42, X92)) → goalF_out_gaa(s(T16), T42, T43)
goalF_in_gaa(s(T16), T42, T46) → U8_gaa(T16, T42, T46, s2lA_in_ga(T16, T41))
U8_gaa(T16, T42, T46, s2lA_out_ga(T16, T41)) → U9_gaa(T16, T42, T46, appendD_in_agaa(T44, T41, T42, T45))
U9_gaa(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → U10_gaa(T16, T42, T46, lastC_in_ag(T46, T45))
lastC_in_ag(T85, .(T85, [])) → lastC_out_ag(T85, .(T85, []))
lastC_in_ag(T95, .(T93, T96)) → U3_ag(T95, T93, T96, lastC_in_ag(T95, T96))
U3_ag(T95, T93, T96, lastC_out_ag(T95, T96)) → lastC_out_ag(T95, .(T93, T96))
U10_gaa(T16, T42, T46, lastC_out_ag(T46, T45)) → goalF_out_gaa(s(T16), T42, T46)
goalF_in_gaa(0, T111, T112) → U11_gaa(T111, T112, appendE_in_aa(T111, X177))
appendE_in_aa(T122, .(T122, [])) → appendE_out_aa(T122, .(T122, []))
U11_gaa(T111, T112, appendE_out_aa(T111, X177)) → goalF_out_gaa(0, T111, T112)
goalF_in_gaa(0, T111, T116) → U12_gaa(T111, T116, appendE_in_aa(T111, T115))
U12_gaa(T111, T116, appendE_out_aa(T111, T115)) → U13_gaa(T111, T116, lastC_in_ag(T116, T115))
U13_gaa(T111, T116, lastC_out_ag(T116, T115)) → goalF_out_gaa(0, T111, T116)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
goalF_in_gaa(s(T16), T10, T11) → U5_gaa(T16, T10, T11, s2lA_in_ga(T16, X32))
s2lA_in_ga(s(T24), .(X66, X67)) → U1_ga(T24, X66, X67, s2lA_in_ga(T24, X67))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T24, X66, X67, s2lA_out_ga(T24, X67)) → s2lA_out_ga(s(T24), .(X66, X67))
U5_gaa(T16, T10, T11, s2lA_out_ga(T16, X32)) → goalF_out_gaa(s(T16), T10, T11)
goalF_in_gaa(s(T16), T42, T43) → U6_gaa(T16, T42, T43, s2lA_in_ga(T16, T41))
U6_gaa(T16, T42, T43, s2lA_out_ga(T16, T41)) → U7_gaa(T16, T42, T43, appendD_in_agaa(X93, T41, T42, X92))
appendD_in_agaa(X117, T57, T58, .(X117, X118)) → U4_agaa(X117, T57, T58, X118, appendB_in_gaa(T57, T58, X118))
appendB_in_gaa([], T65, .(T65, [])) → appendB_out_gaa([], T65, .(T65, []))
appendB_in_gaa(.(T72, T75), T76, .(T72, X140)) → U2_gaa(T72, T75, T76, X140, appendB_in_gaa(T75, T76, X140))
U2_gaa(T72, T75, T76, X140, appendB_out_gaa(T75, T76, X140)) → appendB_out_gaa(.(T72, T75), T76, .(T72, X140))
U4_agaa(X117, T57, T58, X118, appendB_out_gaa(T57, T58, X118)) → appendD_out_agaa(X117, T57, T58, .(X117, X118))
U7_gaa(T16, T42, T43, appendD_out_agaa(X93, T41, T42, X92)) → goalF_out_gaa(s(T16), T42, T43)
goalF_in_gaa(s(T16), T42, T46) → U8_gaa(T16, T42, T46, s2lA_in_ga(T16, T41))
U8_gaa(T16, T42, T46, s2lA_out_ga(T16, T41)) → U9_gaa(T16, T42, T46, appendD_in_agaa(T44, T41, T42, T45))
U9_gaa(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → U10_gaa(T16, T42, T46, lastC_in_ag(T46, T45))
lastC_in_ag(T85, .(T85, [])) → lastC_out_ag(T85, .(T85, []))
lastC_in_ag(T95, .(T93, T96)) → U3_ag(T95, T93, T96, lastC_in_ag(T95, T96))
U3_ag(T95, T93, T96, lastC_out_ag(T95, T96)) → lastC_out_ag(T95, .(T93, T96))
U10_gaa(T16, T42, T46, lastC_out_ag(T46, T45)) → goalF_out_gaa(s(T16), T42, T46)
goalF_in_gaa(0, T111, T112) → U11_gaa(T111, T112, appendE_in_aa(T111, X177))
appendE_in_aa(T122, .(T122, [])) → appendE_out_aa(T122, .(T122, []))
U11_gaa(T111, T112, appendE_out_aa(T111, X177)) → goalF_out_gaa(0, T111, T112)
goalF_in_gaa(0, T111, T116) → U12_gaa(T111, T116, appendE_in_aa(T111, T115))
U12_gaa(T111, T116, appendE_out_aa(T111, T115)) → U13_gaa(T111, T116, lastC_in_ag(T116, T115))
U13_gaa(T111, T116, lastC_out_ag(T116, T115)) → goalF_out_gaa(0, T111, T116)
GOALF_IN_GAA(s(T16), T10, T11) → U5_GAA(T16, T10, T11, s2lA_in_ga(T16, X32))
GOALF_IN_GAA(s(T16), T10, T11) → S2LA_IN_GA(T16, X32)
S2LA_IN_GA(s(T24), .(X66, X67)) → U1_GA(T24, X66, X67, s2lA_in_ga(T24, X67))
S2LA_IN_GA(s(T24), .(X66, X67)) → S2LA_IN_GA(T24, X67)
GOALF_IN_GAA(s(T16), T42, T43) → U6_GAA(T16, T42, T43, s2lA_in_ga(T16, T41))
U6_GAA(T16, T42, T43, s2lA_out_ga(T16, T41)) → U7_GAA(T16, T42, T43, appendD_in_agaa(X93, T41, T42, X92))
U6_GAA(T16, T42, T43, s2lA_out_ga(T16, T41)) → APPENDD_IN_AGAA(X93, T41, T42, X92)
APPENDD_IN_AGAA(X117, T57, T58, .(X117, X118)) → U4_AGAA(X117, T57, T58, X118, appendB_in_gaa(T57, T58, X118))
APPENDD_IN_AGAA(X117, T57, T58, .(X117, X118)) → APPENDB_IN_GAA(T57, T58, X118)
APPENDB_IN_GAA(.(T72, T75), T76, .(T72, X140)) → U2_GAA(T72, T75, T76, X140, appendB_in_gaa(T75, T76, X140))
APPENDB_IN_GAA(.(T72, T75), T76, .(T72, X140)) → APPENDB_IN_GAA(T75, T76, X140)
GOALF_IN_GAA(s(T16), T42, T46) → U8_GAA(T16, T42, T46, s2lA_in_ga(T16, T41))
U8_GAA(T16, T42, T46, s2lA_out_ga(T16, T41)) → U9_GAA(T16, T42, T46, appendD_in_agaa(T44, T41, T42, T45))
U8_GAA(T16, T42, T46, s2lA_out_ga(T16, T41)) → APPENDD_IN_AGAA(T44, T41, T42, T45)
U9_GAA(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → U10_GAA(T16, T42, T46, lastC_in_ag(T46, T45))
U9_GAA(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → LASTC_IN_AG(T46, T45)
LASTC_IN_AG(T95, .(T93, T96)) → U3_AG(T95, T93, T96, lastC_in_ag(T95, T96))
LASTC_IN_AG(T95, .(T93, T96)) → LASTC_IN_AG(T95, T96)
GOALF_IN_GAA(0, T111, T112) → U11_GAA(T111, T112, appendE_in_aa(T111, X177))
GOALF_IN_GAA(0, T111, T112) → APPENDE_IN_AA(T111, X177)
GOALF_IN_GAA(0, T111, T116) → U12_GAA(T111, T116, appendE_in_aa(T111, T115))
U12_GAA(T111, T116, appendE_out_aa(T111, T115)) → U13_GAA(T111, T116, lastC_in_ag(T116, T115))
U12_GAA(T111, T116, appendE_out_aa(T111, T115)) → LASTC_IN_AG(T116, T115)
goalF_in_gaa(s(T16), T10, T11) → U5_gaa(T16, T10, T11, s2lA_in_ga(T16, X32))
s2lA_in_ga(s(T24), .(X66, X67)) → U1_ga(T24, X66, X67, s2lA_in_ga(T24, X67))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T24, X66, X67, s2lA_out_ga(T24, X67)) → s2lA_out_ga(s(T24), .(X66, X67))
U5_gaa(T16, T10, T11, s2lA_out_ga(T16, X32)) → goalF_out_gaa(s(T16), T10, T11)
goalF_in_gaa(s(T16), T42, T43) → U6_gaa(T16, T42, T43, s2lA_in_ga(T16, T41))
U6_gaa(T16, T42, T43, s2lA_out_ga(T16, T41)) → U7_gaa(T16, T42, T43, appendD_in_agaa(X93, T41, T42, X92))
appendD_in_agaa(X117, T57, T58, .(X117, X118)) → U4_agaa(X117, T57, T58, X118, appendB_in_gaa(T57, T58, X118))
appendB_in_gaa([], T65, .(T65, [])) → appendB_out_gaa([], T65, .(T65, []))
appendB_in_gaa(.(T72, T75), T76, .(T72, X140)) → U2_gaa(T72, T75, T76, X140, appendB_in_gaa(T75, T76, X140))
U2_gaa(T72, T75, T76, X140, appendB_out_gaa(T75, T76, X140)) → appendB_out_gaa(.(T72, T75), T76, .(T72, X140))
U4_agaa(X117, T57, T58, X118, appendB_out_gaa(T57, T58, X118)) → appendD_out_agaa(X117, T57, T58, .(X117, X118))
U7_gaa(T16, T42, T43, appendD_out_agaa(X93, T41, T42, X92)) → goalF_out_gaa(s(T16), T42, T43)
goalF_in_gaa(s(T16), T42, T46) → U8_gaa(T16, T42, T46, s2lA_in_ga(T16, T41))
U8_gaa(T16, T42, T46, s2lA_out_ga(T16, T41)) → U9_gaa(T16, T42, T46, appendD_in_agaa(T44, T41, T42, T45))
U9_gaa(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → U10_gaa(T16, T42, T46, lastC_in_ag(T46, T45))
lastC_in_ag(T85, .(T85, [])) → lastC_out_ag(T85, .(T85, []))
lastC_in_ag(T95, .(T93, T96)) → U3_ag(T95, T93, T96, lastC_in_ag(T95, T96))
U3_ag(T95, T93, T96, lastC_out_ag(T95, T96)) → lastC_out_ag(T95, .(T93, T96))
U10_gaa(T16, T42, T46, lastC_out_ag(T46, T45)) → goalF_out_gaa(s(T16), T42, T46)
goalF_in_gaa(0, T111, T112) → U11_gaa(T111, T112, appendE_in_aa(T111, X177))
appendE_in_aa(T122, .(T122, [])) → appendE_out_aa(T122, .(T122, []))
U11_gaa(T111, T112, appendE_out_aa(T111, X177)) → goalF_out_gaa(0, T111, T112)
goalF_in_gaa(0, T111, T116) → U12_gaa(T111, T116, appendE_in_aa(T111, T115))
U12_gaa(T111, T116, appendE_out_aa(T111, T115)) → U13_gaa(T111, T116, lastC_in_ag(T116, T115))
U13_gaa(T111, T116, lastC_out_ag(T116, T115)) → goalF_out_gaa(0, T111, T116)
GOALF_IN_GAA(s(T16), T10, T11) → U5_GAA(T16, T10, T11, s2lA_in_ga(T16, X32))
GOALF_IN_GAA(s(T16), T10, T11) → S2LA_IN_GA(T16, X32)
S2LA_IN_GA(s(T24), .(X66, X67)) → U1_GA(T24, X66, X67, s2lA_in_ga(T24, X67))
S2LA_IN_GA(s(T24), .(X66, X67)) → S2LA_IN_GA(T24, X67)
GOALF_IN_GAA(s(T16), T42, T43) → U6_GAA(T16, T42, T43, s2lA_in_ga(T16, T41))
U6_GAA(T16, T42, T43, s2lA_out_ga(T16, T41)) → U7_GAA(T16, T42, T43, appendD_in_agaa(X93, T41, T42, X92))
U6_GAA(T16, T42, T43, s2lA_out_ga(T16, T41)) → APPENDD_IN_AGAA(X93, T41, T42, X92)
APPENDD_IN_AGAA(X117, T57, T58, .(X117, X118)) → U4_AGAA(X117, T57, T58, X118, appendB_in_gaa(T57, T58, X118))
APPENDD_IN_AGAA(X117, T57, T58, .(X117, X118)) → APPENDB_IN_GAA(T57, T58, X118)
APPENDB_IN_GAA(.(T72, T75), T76, .(T72, X140)) → U2_GAA(T72, T75, T76, X140, appendB_in_gaa(T75, T76, X140))
APPENDB_IN_GAA(.(T72, T75), T76, .(T72, X140)) → APPENDB_IN_GAA(T75, T76, X140)
GOALF_IN_GAA(s(T16), T42, T46) → U8_GAA(T16, T42, T46, s2lA_in_ga(T16, T41))
U8_GAA(T16, T42, T46, s2lA_out_ga(T16, T41)) → U9_GAA(T16, T42, T46, appendD_in_agaa(T44, T41, T42, T45))
U8_GAA(T16, T42, T46, s2lA_out_ga(T16, T41)) → APPENDD_IN_AGAA(T44, T41, T42, T45)
U9_GAA(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → U10_GAA(T16, T42, T46, lastC_in_ag(T46, T45))
U9_GAA(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → LASTC_IN_AG(T46, T45)
LASTC_IN_AG(T95, .(T93, T96)) → U3_AG(T95, T93, T96, lastC_in_ag(T95, T96))
LASTC_IN_AG(T95, .(T93, T96)) → LASTC_IN_AG(T95, T96)
GOALF_IN_GAA(0, T111, T112) → U11_GAA(T111, T112, appendE_in_aa(T111, X177))
GOALF_IN_GAA(0, T111, T112) → APPENDE_IN_AA(T111, X177)
GOALF_IN_GAA(0, T111, T116) → U12_GAA(T111, T116, appendE_in_aa(T111, T115))
U12_GAA(T111, T116, appendE_out_aa(T111, T115)) → U13_GAA(T111, T116, lastC_in_ag(T116, T115))
U12_GAA(T111, T116, appendE_out_aa(T111, T115)) → LASTC_IN_AG(T116, T115)
goalF_in_gaa(s(T16), T10, T11) → U5_gaa(T16, T10, T11, s2lA_in_ga(T16, X32))
s2lA_in_ga(s(T24), .(X66, X67)) → U1_ga(T24, X66, X67, s2lA_in_ga(T24, X67))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T24, X66, X67, s2lA_out_ga(T24, X67)) → s2lA_out_ga(s(T24), .(X66, X67))
U5_gaa(T16, T10, T11, s2lA_out_ga(T16, X32)) → goalF_out_gaa(s(T16), T10, T11)
goalF_in_gaa(s(T16), T42, T43) → U6_gaa(T16, T42, T43, s2lA_in_ga(T16, T41))
U6_gaa(T16, T42, T43, s2lA_out_ga(T16, T41)) → U7_gaa(T16, T42, T43, appendD_in_agaa(X93, T41, T42, X92))
appendD_in_agaa(X117, T57, T58, .(X117, X118)) → U4_agaa(X117, T57, T58, X118, appendB_in_gaa(T57, T58, X118))
appendB_in_gaa([], T65, .(T65, [])) → appendB_out_gaa([], T65, .(T65, []))
appendB_in_gaa(.(T72, T75), T76, .(T72, X140)) → U2_gaa(T72, T75, T76, X140, appendB_in_gaa(T75, T76, X140))
U2_gaa(T72, T75, T76, X140, appendB_out_gaa(T75, T76, X140)) → appendB_out_gaa(.(T72, T75), T76, .(T72, X140))
U4_agaa(X117, T57, T58, X118, appendB_out_gaa(T57, T58, X118)) → appendD_out_agaa(X117, T57, T58, .(X117, X118))
U7_gaa(T16, T42, T43, appendD_out_agaa(X93, T41, T42, X92)) → goalF_out_gaa(s(T16), T42, T43)
goalF_in_gaa(s(T16), T42, T46) → U8_gaa(T16, T42, T46, s2lA_in_ga(T16, T41))
U8_gaa(T16, T42, T46, s2lA_out_ga(T16, T41)) → U9_gaa(T16, T42, T46, appendD_in_agaa(T44, T41, T42, T45))
U9_gaa(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → U10_gaa(T16, T42, T46, lastC_in_ag(T46, T45))
lastC_in_ag(T85, .(T85, [])) → lastC_out_ag(T85, .(T85, []))
lastC_in_ag(T95, .(T93, T96)) → U3_ag(T95, T93, T96, lastC_in_ag(T95, T96))
U3_ag(T95, T93, T96, lastC_out_ag(T95, T96)) → lastC_out_ag(T95, .(T93, T96))
U10_gaa(T16, T42, T46, lastC_out_ag(T46, T45)) → goalF_out_gaa(s(T16), T42, T46)
goalF_in_gaa(0, T111, T112) → U11_gaa(T111, T112, appendE_in_aa(T111, X177))
appendE_in_aa(T122, .(T122, [])) → appendE_out_aa(T122, .(T122, []))
U11_gaa(T111, T112, appendE_out_aa(T111, X177)) → goalF_out_gaa(0, T111, T112)
goalF_in_gaa(0, T111, T116) → U12_gaa(T111, T116, appendE_in_aa(T111, T115))
U12_gaa(T111, T116, appendE_out_aa(T111, T115)) → U13_gaa(T111, T116, lastC_in_ag(T116, T115))
U13_gaa(T111, T116, lastC_out_ag(T116, T115)) → goalF_out_gaa(0, T111, T116)
LASTC_IN_AG(T95, .(T93, T96)) → LASTC_IN_AG(T95, T96)
goalF_in_gaa(s(T16), T10, T11) → U5_gaa(T16, T10, T11, s2lA_in_ga(T16, X32))
s2lA_in_ga(s(T24), .(X66, X67)) → U1_ga(T24, X66, X67, s2lA_in_ga(T24, X67))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T24, X66, X67, s2lA_out_ga(T24, X67)) → s2lA_out_ga(s(T24), .(X66, X67))
U5_gaa(T16, T10, T11, s2lA_out_ga(T16, X32)) → goalF_out_gaa(s(T16), T10, T11)
goalF_in_gaa(s(T16), T42, T43) → U6_gaa(T16, T42, T43, s2lA_in_ga(T16, T41))
U6_gaa(T16, T42, T43, s2lA_out_ga(T16, T41)) → U7_gaa(T16, T42, T43, appendD_in_agaa(X93, T41, T42, X92))
appendD_in_agaa(X117, T57, T58, .(X117, X118)) → U4_agaa(X117, T57, T58, X118, appendB_in_gaa(T57, T58, X118))
appendB_in_gaa([], T65, .(T65, [])) → appendB_out_gaa([], T65, .(T65, []))
appendB_in_gaa(.(T72, T75), T76, .(T72, X140)) → U2_gaa(T72, T75, T76, X140, appendB_in_gaa(T75, T76, X140))
U2_gaa(T72, T75, T76, X140, appendB_out_gaa(T75, T76, X140)) → appendB_out_gaa(.(T72, T75), T76, .(T72, X140))
U4_agaa(X117, T57, T58, X118, appendB_out_gaa(T57, T58, X118)) → appendD_out_agaa(X117, T57, T58, .(X117, X118))
U7_gaa(T16, T42, T43, appendD_out_agaa(X93, T41, T42, X92)) → goalF_out_gaa(s(T16), T42, T43)
goalF_in_gaa(s(T16), T42, T46) → U8_gaa(T16, T42, T46, s2lA_in_ga(T16, T41))
U8_gaa(T16, T42, T46, s2lA_out_ga(T16, T41)) → U9_gaa(T16, T42, T46, appendD_in_agaa(T44, T41, T42, T45))
U9_gaa(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → U10_gaa(T16, T42, T46, lastC_in_ag(T46, T45))
lastC_in_ag(T85, .(T85, [])) → lastC_out_ag(T85, .(T85, []))
lastC_in_ag(T95, .(T93, T96)) → U3_ag(T95, T93, T96, lastC_in_ag(T95, T96))
U3_ag(T95, T93, T96, lastC_out_ag(T95, T96)) → lastC_out_ag(T95, .(T93, T96))
U10_gaa(T16, T42, T46, lastC_out_ag(T46, T45)) → goalF_out_gaa(s(T16), T42, T46)
goalF_in_gaa(0, T111, T112) → U11_gaa(T111, T112, appendE_in_aa(T111, X177))
appendE_in_aa(T122, .(T122, [])) → appendE_out_aa(T122, .(T122, []))
U11_gaa(T111, T112, appendE_out_aa(T111, X177)) → goalF_out_gaa(0, T111, T112)
goalF_in_gaa(0, T111, T116) → U12_gaa(T111, T116, appendE_in_aa(T111, T115))
U12_gaa(T111, T116, appendE_out_aa(T111, T115)) → U13_gaa(T111, T116, lastC_in_ag(T116, T115))
U13_gaa(T111, T116, lastC_out_ag(T116, T115)) → goalF_out_gaa(0, T111, T116)
LASTC_IN_AG(T95, .(T93, T96)) → LASTC_IN_AG(T95, T96)
LASTC_IN_AG(.(T96)) → LASTC_IN_AG(T96)
From the DPs we obtained the following set of size-change graphs:
APPENDB_IN_GAA(.(T72, T75), T76, .(T72, X140)) → APPENDB_IN_GAA(T75, T76, X140)
goalF_in_gaa(s(T16), T10, T11) → U5_gaa(T16, T10, T11, s2lA_in_ga(T16, X32))
s2lA_in_ga(s(T24), .(X66, X67)) → U1_ga(T24, X66, X67, s2lA_in_ga(T24, X67))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T24, X66, X67, s2lA_out_ga(T24, X67)) → s2lA_out_ga(s(T24), .(X66, X67))
U5_gaa(T16, T10, T11, s2lA_out_ga(T16, X32)) → goalF_out_gaa(s(T16), T10, T11)
goalF_in_gaa(s(T16), T42, T43) → U6_gaa(T16, T42, T43, s2lA_in_ga(T16, T41))
U6_gaa(T16, T42, T43, s2lA_out_ga(T16, T41)) → U7_gaa(T16, T42, T43, appendD_in_agaa(X93, T41, T42, X92))
appendD_in_agaa(X117, T57, T58, .(X117, X118)) → U4_agaa(X117, T57, T58, X118, appendB_in_gaa(T57, T58, X118))
appendB_in_gaa([], T65, .(T65, [])) → appendB_out_gaa([], T65, .(T65, []))
appendB_in_gaa(.(T72, T75), T76, .(T72, X140)) → U2_gaa(T72, T75, T76, X140, appendB_in_gaa(T75, T76, X140))
U2_gaa(T72, T75, T76, X140, appendB_out_gaa(T75, T76, X140)) → appendB_out_gaa(.(T72, T75), T76, .(T72, X140))
U4_agaa(X117, T57, T58, X118, appendB_out_gaa(T57, T58, X118)) → appendD_out_agaa(X117, T57, T58, .(X117, X118))
U7_gaa(T16, T42, T43, appendD_out_agaa(X93, T41, T42, X92)) → goalF_out_gaa(s(T16), T42, T43)
goalF_in_gaa(s(T16), T42, T46) → U8_gaa(T16, T42, T46, s2lA_in_ga(T16, T41))
U8_gaa(T16, T42, T46, s2lA_out_ga(T16, T41)) → U9_gaa(T16, T42, T46, appendD_in_agaa(T44, T41, T42, T45))
U9_gaa(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → U10_gaa(T16, T42, T46, lastC_in_ag(T46, T45))
lastC_in_ag(T85, .(T85, [])) → lastC_out_ag(T85, .(T85, []))
lastC_in_ag(T95, .(T93, T96)) → U3_ag(T95, T93, T96, lastC_in_ag(T95, T96))
U3_ag(T95, T93, T96, lastC_out_ag(T95, T96)) → lastC_out_ag(T95, .(T93, T96))
U10_gaa(T16, T42, T46, lastC_out_ag(T46, T45)) → goalF_out_gaa(s(T16), T42, T46)
goalF_in_gaa(0, T111, T112) → U11_gaa(T111, T112, appendE_in_aa(T111, X177))
appendE_in_aa(T122, .(T122, [])) → appendE_out_aa(T122, .(T122, []))
U11_gaa(T111, T112, appendE_out_aa(T111, X177)) → goalF_out_gaa(0, T111, T112)
goalF_in_gaa(0, T111, T116) → U12_gaa(T111, T116, appendE_in_aa(T111, T115))
U12_gaa(T111, T116, appendE_out_aa(T111, T115)) → U13_gaa(T111, T116, lastC_in_ag(T116, T115))
U13_gaa(T111, T116, lastC_out_ag(T116, T115)) → goalF_out_gaa(0, T111, T116)
APPENDB_IN_GAA(.(T72, T75), T76, .(T72, X140)) → APPENDB_IN_GAA(T75, T76, X140)
APPENDB_IN_GAA(.(T75)) → APPENDB_IN_GAA(T75)
From the DPs we obtained the following set of size-change graphs:
S2LA_IN_GA(s(T24), .(X66, X67)) → S2LA_IN_GA(T24, X67)
goalF_in_gaa(s(T16), T10, T11) → U5_gaa(T16, T10, T11, s2lA_in_ga(T16, X32))
s2lA_in_ga(s(T24), .(X66, X67)) → U1_ga(T24, X66, X67, s2lA_in_ga(T24, X67))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T24, X66, X67, s2lA_out_ga(T24, X67)) → s2lA_out_ga(s(T24), .(X66, X67))
U5_gaa(T16, T10, T11, s2lA_out_ga(T16, X32)) → goalF_out_gaa(s(T16), T10, T11)
goalF_in_gaa(s(T16), T42, T43) → U6_gaa(T16, T42, T43, s2lA_in_ga(T16, T41))
U6_gaa(T16, T42, T43, s2lA_out_ga(T16, T41)) → U7_gaa(T16, T42, T43, appendD_in_agaa(X93, T41, T42, X92))
appendD_in_agaa(X117, T57, T58, .(X117, X118)) → U4_agaa(X117, T57, T58, X118, appendB_in_gaa(T57, T58, X118))
appendB_in_gaa([], T65, .(T65, [])) → appendB_out_gaa([], T65, .(T65, []))
appendB_in_gaa(.(T72, T75), T76, .(T72, X140)) → U2_gaa(T72, T75, T76, X140, appendB_in_gaa(T75, T76, X140))
U2_gaa(T72, T75, T76, X140, appendB_out_gaa(T75, T76, X140)) → appendB_out_gaa(.(T72, T75), T76, .(T72, X140))
U4_agaa(X117, T57, T58, X118, appendB_out_gaa(T57, T58, X118)) → appendD_out_agaa(X117, T57, T58, .(X117, X118))
U7_gaa(T16, T42, T43, appendD_out_agaa(X93, T41, T42, X92)) → goalF_out_gaa(s(T16), T42, T43)
goalF_in_gaa(s(T16), T42, T46) → U8_gaa(T16, T42, T46, s2lA_in_ga(T16, T41))
U8_gaa(T16, T42, T46, s2lA_out_ga(T16, T41)) → U9_gaa(T16, T42, T46, appendD_in_agaa(T44, T41, T42, T45))
U9_gaa(T16, T42, T46, appendD_out_agaa(T44, T41, T42, T45)) → U10_gaa(T16, T42, T46, lastC_in_ag(T46, T45))
lastC_in_ag(T85, .(T85, [])) → lastC_out_ag(T85, .(T85, []))
lastC_in_ag(T95, .(T93, T96)) → U3_ag(T95, T93, T96, lastC_in_ag(T95, T96))
U3_ag(T95, T93, T96, lastC_out_ag(T95, T96)) → lastC_out_ag(T95, .(T93, T96))
U10_gaa(T16, T42, T46, lastC_out_ag(T46, T45)) → goalF_out_gaa(s(T16), T42, T46)
goalF_in_gaa(0, T111, T112) → U11_gaa(T111, T112, appendE_in_aa(T111, X177))
appendE_in_aa(T122, .(T122, [])) → appendE_out_aa(T122, .(T122, []))
U11_gaa(T111, T112, appendE_out_aa(T111, X177)) → goalF_out_gaa(0, T111, T112)
goalF_in_gaa(0, T111, T116) → U12_gaa(T111, T116, appendE_in_aa(T111, T115))
U12_gaa(T111, T116, appendE_out_aa(T111, T115)) → U13_gaa(T111, T116, lastC_in_ag(T116, T115))
U13_gaa(T111, T116, lastC_out_ag(T116, T115)) → goalF_out_gaa(0, T111, T116)
S2LA_IN_GA(s(T24), .(X66, X67)) → S2LA_IN_GA(T24, X67)
S2LA_IN_GA(s(T24)) → S2LA_IN_GA(T24)
From the DPs we obtained the following set of size-change graphs: